Nuprl Lemma : free-from-atom-IdLnk
11,40
postcript
pdf
a
:Atom1,
l
:IdLnk.
l
:IdLnk||
a
latex
Definitions
x
:
A
.
B
(
x
)
,
IdLnk
,
t
T
Lemmas
free-from-atom-Id
,
Id
wf
origin
a:Atom1, l:IdLnk. l:IdLnk||a a:Atom1, l:IdLnk. l:IdLnk||a x:A. B(x)
T